Coq (proof assistant system)

Coq is a theorem proving assistance system. It is one of the core systems used in the field. The main language used in Coq is Gallina. Coq was developed by the PI.R2 team at the French National Institute for Research in Computer Science and Automation, in collaboration with Ecole Polytechnique, the National School of Arts and Crafts, Paris Diderot University, and Paris-Sud University. Formerly, it was also developed in collaboration with the École Normale Supérieure de Lyon. Hugo Herbelin is the de facto development representative of Coq.

For more information about Coq, you can refer to the Coq Wikipedia page(https://ja.wikipedia.org/wiki/Coq).

If you are interested in learning about theorem proving systems and what they can do, you can check out this SlideShare presentation(https://www.slideshare.net/secret/3Q3X3Q3X3Q3X3Q/about-theorem-proving-assistance-system-coq).

Additionally, you may find this article(https://note.com/morikita/n/nf45b6e44964f) from Morikita Publishing helpful in understanding what a theorem proving system is and its capabilities.

Here is a screenshot(https://gyazo.com/ba3b9998bf258aa44a727ab3ff480349) for reference.